$\forall$$i$, $a$, $x$:Id, $X$, $T$:Type, $x_{0}$:$X$, $P$:($X$$\rightarrow$$T$$\rightarrow$Prop).
\\[0ex]Normal($T$)
\\[0ex]$\Rightarrow$ Normal($X$)
\\[0ex]$\Rightarrow$ ($\forall$$x$:$X$. Dec($\exists$$v$:$T$. $P$($x$,$v$)))
\\[0ex]$\Rightarrow$ R{-}Feasible(R{-}pre{-}init1($i$;$x$;$X$;$x_{0}$;$a$;$T$;$P$))